A:Type, I:MaInterface(A), l:IdLnk, tg:Id. gluable(I;l;tg)   

latex

Definitions	Type, t  T, {x:A| B(x)} , Knd, b, Top, left + right, x:AB(x), x:A. B(x), State(ds), x:A  B(x), hasloc(k;i), x. t(x), a:A fp B(a), Id, (x  l), type List, MaInterface(T), IdLnk, S  T, P  Q, ma-interface-dom(I;i), rcv(l,tg), A, ma-interface-locs(I), source(l), , Atom$n, gluable(I;l;tg)
Lemmas	lsrc wf, ma-interface-locs wf, not wf, rcv wf, ma-interface-dom wf, l member wf, Id wf, fpf wf, Knd wf, assert wf, hasloc wf, decl-state wf, top wf